COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∧I INDUCTION1[P←λx.∀u.LIST FLAT(x,u)]
C00005 ENDMK
C⊗;
∧I INDUCTION1[P←λx.∀u.LIST FLAT(x,u)];
∀e FLAT x u;
distrib λX.=(FLAT(x,u),X) 2:#2;
assume ATOM x;
taut FLAT(x,u) = CONS(x,u) 2 3 4;
∀e CONS2 x u;
tauteq LIST 5:#1 5 6;
∀I 7 u;
⊃i 4 8;
∀i 9 x;
assume ¬ATOM x;
taut FLAT(x,u) = FLAT(CAR x,FLAT(CDR x,u)) 2 3 11;
assume ∀u.LIST FLAT(CAR x,u);
assume ∀u.LIST FLAT(CDR x,u);
∀e 14 u;
∀e 13 FLAT(CDR x,u);
tauteq LIST FLAT(x,u) 12 15 16;
∀i 17 u;
⊃i 14 18;
⊃i 13 19;
⊃i 11 20;
taut 1:#1#2#1 21;
∀i 22 x;
taut 1:#2 1 10 23;